Nuprl Lemma : f2f+AckDcdr_wf
11,40
postcript
pdf
es
:ES,
ff
:FIFO,
f2f+
:F2F+-decls. ack_dcdr
e
:E
Dec(is_ack (
e
))
latex
Definitions
t
.2
,
t
.1
,
ack_dcdr
,
is_ack
,
t
T
,
x
:
A
.
B
(
x
)
,
F2F+-decls
Lemmas
event
system
wf
,
FIFO
wf
,
F2F+-decls
wf
origin
es:ES, ff:FIFO, f2f+:F2F+-decls. ack_dcdr 
e:E
Dec(is_ack (e)) es:ES, ff:FIFO, f2f+:F2F+-decls. ack_dcdr e:EDec(is_ack (e)) Tx:A. B(x)